| 1: | plus(x,0) | → x | |
| 2: | plus(0,y) | → y | |
| 3: | plus(s(x),y) | → s(plus(x,y)) | |
| 4: | times(0,y) | → 0 | |
| 5: | times(s(0),y) | → y | |
| 6: | times(s(x),y) | → plus(y,times(x,y)) | |
| 7: | div(0,y) | → 0 | |
| 8: | div(x,y) | → quot(x,y,y) | |
| 9: | quot(0,s(y),z) | → 0 | |
| 10: | quot(s(x),s(y),z) | → quot(x,y,z) | |
| 11: | quot(x,0,s(z)) | → s(div(x,s(z))) | |
| 12: | div(div(x,y),z) | → div(x,times(y,z)) | |
| 13: | eq(0,0) | → true | |
| 14: | eq(s(x),0) | → false | |
| 15: | eq(0,s(y)) | → false | |
| 16: | eq(s(x),s(y)) | → eq(x,y) | |
| 17: | divides(y,x) | → eq(x,times(div(x,y),y)) | |
| 18: | prime(s(s(x))) | → pr(s(s(x)),s(x)) | |
| 19: | pr(x,s(0)) | → true | |
| 20: | pr(x,s(s(y))) | → if(divides(s(s(y)),x),x,s(y)) | |
| 21: | if(true,x,y) | → false | |
| 22: | if(false,x,y) | → pr(x,y) | |
| 23: | PLUS(s(x),y) | → PLUS(x,y) | |
| 24: | TIMES(s(x),y) | → PLUS(y,times(x,y)) | |
| 25: | TIMES(s(x),y) | → TIMES(x,y) | |
| 26: | DIV(x,y) | → QUOT(x,y,y) | |
| 27: | QUOT(s(x),s(y),z) | → QUOT(x,y,z) | |
| 28: | QUOT(x,0,s(z)) | → DIV(x,s(z)) | |
| 29: | DIV(div(x,y),z) | → DIV(x,times(y,z)) | |
| 30: | DIV(div(x,y),z) | → TIMES(y,z) | |
| 31: | EQ(s(x),s(y)) | → EQ(x,y) | |
| 32: | DIVIDES(y,x) | → EQ(x,times(div(x,y),y)) | |
| 33: | DIVIDES(y,x) | → TIMES(div(x,y),y) | |
| 34: | DIVIDES(y,x) | → DIV(x,y) | |
| 35: | PRIME(s(s(x))) | → PR(s(s(x)),s(x)) | |
| 36: | PR(x,s(s(y))) | → IF(divides(s(s(y)),x),x,s(y)) | |
| 37: | PR(x,s(s(y))) | → DIVIDES(s(s(y)),x) | |
| 38: | IF(false,x,y) | → PR(x,y) | |